COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Mailed to CSD.MOSTOW 18:40 18-Nov
C00007 ENDMK
C⊗;
Mailed to CSD.MOSTOW 18:40 18-Nov
Formal Approach
In-1  = {xεA | Q(x) }
Out-1 = {yεB | ∃x. Q(x) & f(x,y) & P(y) }

You may view "Q" as a generator of x's, which enter a box whose output
will be the set Out-1. This output is generated by first determining
those y which satisfy f(x,y) [ie there is a function F which takes
elements of Q onto sets of these y's -- F: A => p(B)... then
f(x,y) <=> y ε F(x) [[p(X) ≡ the powerset of X]] ],
and then restricting this set of y's, using the predicate P.

This test P may be moved forward in this process, and transformed into
a predicate, π, which takes members of A. (Note P took members of B.)

Define π(x) ≡ ∃y. P(y) & f(x,y) .  [Actually, this could be
iff Q(x) => ∃y. P(y) & f(x,y), but we'll just assume π is ony applied
to members of Q.
Given this definition, we imagine a process which takes members of Q,
filters these using π, and then transforms these using f, and returns this
set, Out-2, as output.  Formally,
Out-2 = {yεB | ∃x. Q(x) & π(x) & f(x,y) }

To satisfy the objective of not throwing out any legitimate member (of Out-1)
by moving this test earlier, we need only show Out-1 ⊂ Out-2.
So take any y1 ε Out-1 -- ie ∃x. Q(x) & f(x,y1) & P(y1).
Chose x1 which is that existential member.  As P(y1) & f(x1,y1), π(x1) is true.
This was all we needed to show y1 ε Out-2, as we have x1 s.t.
Q(x1) & π(x1) & f(x1,y1).  QED

 ... ----- ... ----- ... ----- ...

Now let's consider nice cases of this movement:
Notice this π(x) ≡ ∃y. P(y) & f(x,y)  definition is incredibly cautious --
telling us to leave in every x which has ANY chance, however small, of ever
emerging (after being f-transformed).  
It is, of course, possible that some y1 emerging from the second process does
NOT satisfy P. For example, take A = B = Natural Numbers, and Q(x)≡T and
let f(x,y) ≡ y>x.
Taking P(y) ≡ y<2, it is clear that Out-1 = {0, 1}.
π(x) ≡ ∃y. P(y) & f(x,y) means π(x) ≡ ∃y. y<2 & x<y - so π = {0}.
Now Out-2 = {yεNN | ∃x. T & xε{0} & x<y} = {yεNN | x=0 & x<y} = NN.  QED

Notice that this doesn't happen if π(x) ≡ ∀x. ... -- and these two definitions
are equivalent when f happens to be a function [i.e. ∀x.∃!y. f(x,y) ].

Other cases to consider: when one doesn't want to get all of Out-1, but just
some y1 which satisfied this set of constraints. 
I'll think about this tomorrow, if you think it's worth it.

Note this is stored in JACK[RDG,DBL].

Also, do not bother copying my INIT.LISP file - testing it, I found it
doesn't work. You might try <CSD.SMITH>INIT.LISp, but that doesn't have
the critical DATAMEDIA command. To read that in, type
LOAD(<CSD.SMITH>XUTIL.COM)   to LISP's top level; followed by
DATAMEDIA)   . Backspaces will do the write thing from then on.

Russ